This paper applies resolution theorem proving to natural language semantics.The aim is to circumvent the computational complexity triggered by naturallanguage ambiguities like pronoun binding, by interleaving pronoun binding withresolution deduction. Therefore disambiguation is only applied to expressionthat actually occur during derivations.
展开▼